STM: event system typename wf

ABS: EventsWithOrder

STM: EOrder wf

ABS: EventsWithState

STM: EState wf

STM: EState-subtype-EOrder

ABS: EventsWithKinds

STM: EKind wf

ABS: EventsWithValues

STM: EVal wf

ABS: ESAtomAxiom{i:l}(T;V)

ABS: ESMachineAxiom(E;T;V;M;loc;knd;val;when;after;sndr;Trans;Send;Choose)

STM: ESMachineAxiom wf

STM: ESAtomAxiom wf

STM: ESAtomAxiomTrivial

ABS: ES0

STM: event-system0 wf

ABS: old_event_system{i:l}()

ABS: e = e'

STM: es-eq-E wf

STM: assert-es-eq-E

STM: decidable es-E equal

ABS: es-LnkTag-deq

STM: es-LnkTag-deq wf

ABS: case(kind(e))act(a) => f(a)rcv(l,tg) => g(l;tg)

STM: es-kindcase wf

ABS: msgtype(m)

STM: es-msgtype wf

STM: es-valtype-kindtype

ABS: state@i\\x

STM: es-state-without wf

STM: es-state-eta

STM: event system-level-subtype

ABS: mk-es0(E;eq;T;V;M;loc;k;v;w;a;snds;sndr;i;f;prd;cl;p;q)

STM: mk-es0 wf

ABS: mk-eval(E;eq;prd;info;oax;T;w;a;sax;V;v)

STM: mk-eval wf

ABS: AtomFreeDecls(X)

STM: EVal-atom-free wf

STM: EVal-to-ES

ABS: EVal_to_ES{i:l}(e,p)

STM: EVal to ES wf

ABS: state when e\\x

STM: es-state-when-without wf

ABS: state after e\\x

STM: es-state-after-without wf

ABS: e c e'

STM: es-causle wf

STM: es-locl-trans

STM: es-le-trans

STM: es-le-trans2

STM: es-le-trans3

STM: es-index-zero

STM: es-causle-trans

STM: es-causle transitivity

STM: es-le-causle

STM: es-le-total

STM: es-locl-swellfnd

STM: es-causl-wellfnd

STM: es-le-not-locl

STM: es-causal-antireflexive

STM: es-causl-locl

STM: es-causle-le

STM: es-pred-locl

STM: es-le-self

STM: es-pred-le

STM: es-pred-causl

STM: es-sender-causl

STM: es-sender-causle

STM: es-first-implies

STM: es-loc-rcv

STM: es-isrcv-loc

STM: es-hasloc

STM: es-loc-sender

STM: same-sender-index

STM: es-le-iff

STM: es-first-le

STM: es-le-antisymmetric

STM: es-first-unique

STM: es-causl-iff

STM: implies-es-pred

STM: es-le-pred

STM: implies-es-pred2

STM: es-pred-one-one

STM: decidable es-locl

STM: es-next

ABS: e <loc e'

STM: es-bless wf

STM: assert-es-bless

STM: decidable es-le

ABS: es-ble{i:l}(es;e;e')

STM: es-ble wf

STM: assert-es-ble

STM: decidable es-causl

ABS: es-bc{i:l}(es;e;e')

STM: es-bc wf

STM: assert-es-bc

ABS: e=k(v).P(e;v)

ABS: e:rvc(l,tg,v).P(e;v)

ABS: mval(m)

STM: es-mval wf

STM: es-mval-valtype

STM: es-msg-rcvd

ABS: before(e)

STM: es-before wf

STM: es-before wf2

STM: member-es-before

STM: l before-es-before

STM: l before-es-before-iff

ABS: es-init(es;e)

STM: es-init wf

STM: es-init-le

STM: es-first-init

STM: es-loc-init

ABS: [e, e']

STM: es-interval wf

STM: member-es-interval

STM: l before-es-interval

STM: hd-es-interval

STM: es-interval-non-zero

STM: es-interval-nil

STM: es-interval-is-nil

STM: es-interval-last

STM: es-interval-less

STM: es-interval-less-sq

STM: es-interval-eq

STM: es-interval-eq2

STM: es-interval-length-one-one

STM: es-interval-one-one

STM: es-interval-iseg

STM: es-interval-partition

STM: es-interval-select

STM: es-interval wf2

ABS: haslnk(l;e)

STM: es-haslnk wf

STM: assert-es-haslnk

ABS: rcvs(l;before(e'))

STM: es-rcvs wf

STM: member-es-rcvs

ABS: snds(l;before(e))

STM: es-snds wf

STM: member-es-snds

ABS: snds(l, before(e,n))

STM: es-snds-index wf

STM: member-es-snds-index

STM: firstn-before

STM: es-before-decomp

STM: last-es-snds-index

ABS: emsg(e)

STM: es-msg wf

STM: es-msg wf2

STM: es-msg-member-sends

ABS: msgs(l;before(e'))

STM: es-msgs wf

STM: haslink wf2

STM: member-es-msgs

STM: es-fifo-nil

STM: es-fifo

STM: es-after-pred

STM: decl-state-exists

STM: decl-state-subtype

ABS: @i always.P(x)

STM: alle-at1 wf

ABS: @i always.P(x1;x2)

STM: alle-at2 wf

STM: alle-at-iff

STM: alle-at-not-first

STM: es-invariant1

STM: es-invariant2

STM: es-constant1

ABS: e@i.P(e)

STM: existse-at wf

STM: change-lemma

STM: es-first-exists

STM: change-since-init

ABS: ee'.P(e)

STM: existse-le wf

ABS: e<e'.P(e)

STM: existse-before wf

STM: existse-before-iff

STM: decidable existse-before

STM: existse-le-iff

STM: decidable existse-le

ABS: e'e.P(e')

STM: alle-ge wf

ABS: e<e'. P(e)

STM: alle-lt wf

STM: alle-lt-iff

STM: decidable alle-lt

ABS: ee'.P(e)

STM: alle-le wf

STM: alle-le-iff

STM: decidable alle-le

ABS: e[e1,e2).P(e)

STM: alle-between1 wf

STM: alle-between1-true

STM: alle-between1-false

STM: alle-between1 functionality wrt iff

STM: decidable alle-between1

ABS: e[e1,e2).P(e)

STM: existse-between1 wf

STM: existse-between1-true

STM: existse-between1-false

STM: existse-between1 functionality wrt iff

STM: decidable existse-between1

ABS: e[e1,e2].P(e)

STM: alle-between2 wf

STM: alle-between2-true

STM: alle-between2-false

STM: alle-between2 functionality wrt iff

STM: decidable alle-between2

ABS: e[e1,e2].P(e)

STM: existse-between2 wf

STM: existse-between2-false

STM: existse-between2-true

STM: existse-between2 functionality wrt iff

STM: decidable existse-between2

ABS: e(e1,e2].P(e)

STM: existse-between3 wf

STM: existse-between3-false

STM: existse-between3-true

STM: existse-between3 functionality wrt iff

STM: decidable existse-between3

STM: es-subinterval

STM: last-change

ABS: e is first@ i s.t.  e.P(e)

STM: es-first-at wf

STM: es-first-before

STM: es-first-before2

ABS: es-first-at-since(es;i;e;e.R(e);e.P(e))

STM: es-first-at-since wf

STM: previous-event-exists

STM: es-first-at-since-iff

ABS: es-first-at-since'(es;i;e;e.R(e);e.P(e))

STM: es-first-at-since' wf

ABS: e=rcv(l,tg). P(e)

STM: alle-rcv wf

ABS: e=rcv(l,tg). P(e)

STM: existse-rcv wf

STM: es-bound-list

STM: es-bound-list2

STM: es-machine-axiom

STM: atom-free-es-kindtype

STM: atom-free-es-Msg

STM: atom-free-es-valtype

STM: atom-free-es-vartype

STM: atom-free-es-state

STM: atom-free-es-state-without

ABS: e receives a

STM: es-rcv-atom wf

ABS: e sends a

STM: es-send-atom wf

ABS: e sends a to i

STM: es-send-atom-to wf

ABS: e leaks x to e'

ABS: e copies x

STM: state-after-pred

STM: implies-es-atom-axiom

ABS: i >> a

STM: es-atom wf

STM: es-copies wf

STM: es-leaks wf

STM: es-atom-axiom

STM: es-atom-lemma1

STM: es-atom-lemma2

ABS: @i stable state.P(state)  

STM: es-stable wf

STM: stable-implies

STM: stable-implies2

STM: stable-implies3

STM: stable-implies4

STM: last-state-change

STM: last-state-change2

STM: last-state-change3

ABS: es-frame(es;i;L;x;T)

STM: es-frame wf

STM: es-stable-1

STM: es-stable-2

STM: es-stable-3

STM: es-constant-1

ABS: es-responsive(es;l1;tg1;l2;tg2)

STM: es-responsive wf

STM: es-responsive-bijection

ABS: only k(v):B sends [tg,f(s;v)] : T on l

STM: es-only-sender wf

ABS: @i x has type T

STM: vartype-es-type

STM: vartype-es-state-sub

STM: es-state-subtype

STM: state-after-pred-ds

STM: es-when-first

STM: init-p-implies

ABS: usends1-p(es;ds;k;T;l;tg;B;f)

STM: usends1-p wf

ABS: pre-init1-p(es;i;x;X;x0;a;T;P)

STM: pre-init1-p wf

ABS: weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)

STM: weak-precond-send-p wf

ABS: @i locl(a) occurs once

STM: once-p wf

ABS: locl(a) sends [tg,f{AT}(x)] on link l once

STM: send-once-p wf

STM: es-interval-induction

STM: es-interval-induction2

ABS: PossibleEvent(poss)

STM: possible-event wf

ABS: pe-es(e)

STM: pe-es wf

ABS: pe-e(p)

STM: pe-e wf

ABS: pe-state(p)

STM: pe-state wf

ABS: pe-loc(p)

STM: pe-loc wf

ABS: K(P)@e

STM: es-knows wf

STM: es-knows-true

STM: es-knows-knows

STM: es-knows-not

STM: es-knows-trans

STM: es-knows-valid

ABS: e1  e2

STM: poss-le wf

STM: es-knows-stable

ABS: e:s.P(s)@j 

STM: es-simul wf

ABS: es-decls(es;i;ds;da)

STM: es-decls wf

STM: es-decls-iff

STM: es-decls-join-single

ABS: with decls ds dasends on l from e include f(e) and only these for tags in tgs

STM: es-sends-iff wf

ABS: state dsk:A sends [tg, e.f(e):B] on l

STM: es-kind-sends-iff wf

STM: es-sends-iff functionality

ABS: es-update-iff(es;i;x;ds;e.P(e);s.f(s))

STM: es-update-iff wf

ABS: es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))

STM: es-sends-iff2 wf

STM: es-sends-iff2 functionality

ABS: event-info(ds;da)

STM: event-info wf

ABS: es-info(es;e)

STM: es-info wf

ABS: es-hist{i:l}(es;e1;e2)

STM: es-hist wf

STM: member-es-hist

STM: null-es-hist

STM: es-hist-iseg

STM: es-hist-partition

STM: es-hist-last

STM: last-es-hist

STM: es-hist-is-append

STM: es-hist-is-concat

STM: iseg-es-hist

STM: es-hist-one-one

ABS: es-trans-state-from{i:l}(es;ks;g;z;e1;e2)

STM: es-trans-state-from wf

ABS: e2 = first e  e1.P(e)

STM: es-first-since wf

STM: es-first-since functionality wrt iff

STM: alle-between1-not-first-since

STM: alle-between2-not-first-since

STM: es-increasing-sequence

STM: es-increasing-sequence2

ABS: [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b)

STM: es-pstar-q wf

STM: es-pstar-q-trivial

STM: es-pstar-q-le

STM: es-pstar-q functionality wrt implies

STM: es-pstar-q functionality wrt rev implies

STM: es-pstar-q functionality wrt iff

STM: es-pstar-q-partition

ABS: [e1,e2]~([a,b].p(a;b))+

STM: es-pplus wf

STM: es-pplus functionality wrt implies

STM: es-pplus functionality wrt rev implies

STM: es-pplus functionality wrt iff

STM: es-pplus-trivial

STM: es-pplus-le

STM: es-pplus-alle-between2

STM: es-pplus-partition

STM: es-pplus-first-since

STM: es-pplus-first-since-exit

ABS: data(T)

STM: data wf

ABS: secret-table(T)

STM: secret-table wf

ABS: ||tab|| 

STM: st-length wf

ABS: ptr(tab)

STM: st-ptr wf

ABS: st-atom(tab;n)

STM: st-atom wf

ABS: atoms-distinct(tab)

STM: st-atoms-distinct wf

ABS: next(tab)

STM: st-next wf

ABS: key(tab;n)

STM: st-key wf

ABS: data(tab;n)

STM: st-data wf

STM: st-ptr-wf2

ABS: st-lookup(tab;x)

STM: st-lookup wf

STM: st-lookup-property

STM: st-lookup-outl

STM: st-lookup-distinct

ABS: st-key-match(tab;k1;k2)

STM: st-key-match wf

ABS: decrypt(tab;kval)

STM: st-decrypt wf

ABS: encrypt(tab;keyv)

STM: st-encrypt wf

STM: st-length-encrypt

STM: st-atom-encrypt

ABS: ?[x]

STM: cond-to-list wf

ABS: es-secret-server

STM: es-secret-server wf

STM: ss-ptr-non-decreasing

STM: ss-table-length

STM: ss-atom-constant

STM: ss-atoms-distinct

STM: ss-encrypt-unique

ABS: es-seq(es;S)

STM: es-seq wf

STM: send-minimal-lemma

STM: better-send-minimal-lemma